a in dom(M.pre) == a  dom(1of(2of(2of(2of(M))))) 

latex

---

clarification:

a in dom(M.pre) == fpf-dom(IdDeq; a; 1of(2of(2of(2of(M))))) 

latex

Definitions	2of(t), 1of(t), IdDeq, x  dom(f), b
FDL editor aliases	ma-has-pre